@i:k sends only on links in L == e@i. kind(e) = k  (l:IdLnk. (l  L)  sends(l;e) = nil) 

latex

---

clarification:

bframe-p(es;i;k;L)
== alle-at(es;i;e.es-kind(es; e) = k  Knd
== alle-at(es;i;e. (l:IdLnk.
== alle-at(es;i;e. ((l  L  IdLnk)  es-sends(es; l; e) = nil  es-Msg(es) List)) 

latex

Definitions	e@i. P(e), Knd, kind(e), x:A. B(x), P  Q, A, (x  l), IdLnk, s = t, type List, Msg, sends(l;e), nil
FDL editor aliases	bframe-p